(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#equal(@x, @y) → #eq(@x, @y)
#greater(@x, @y) → #ckgt(#compare(@x, @y))
+(@x, @y) → #add(@x, @y)
firstline(@l) → firstline#1(@l)
firstline#1(::(@x, @xs)) → ::(#abs(#0), firstline(@xs))
firstline#1(nil) → nil
lcs(@l1, @l2) → lcs#1(lcstable(@l1, @l2))
lcs#1(@m) → lcs#2(@m)
lcs#2(::(@l1, @_@2)) → lcs#3(@l1)
lcs#2(nil) → #abs(#0)
lcs#3(::(@len, @_@1)) → @len
lcs#3(nil) → #abs(#0)
lcstable(@l1, @l2) → lcstable#1(@l1, @l2)
lcstable#1(::(@x, @xs), @l2) → lcstable#2(lcstable(@xs, @l2), @l2, @x)
lcstable#1(nil, @l2) → ::(firstline(@l2), nil)
lcstable#2(@m, @l2, @x) → lcstable#3(@m, @l2, @x)
lcstable#3(::(@l, @ls), @l2, @x) → ::(newline(@x, @l, @l2), ::(@l, @ls))
lcstable#3(nil, @l2, @x) → nil
max(@a, @b) → max#1(#greater(@a, @b), @a, @b)
max#1(#false, @a, @b) → @b
max#1(#true, @a, @b) → @a
newline(@y, @lastline, @l) → newline#1(@l, @lastline, @y)
newline#1(::(@x, @xs), @lastline, @y) → newline#2(@lastline, @x, @xs, @y)
newline#1(nil, @lastline, @y) → nil
newline#2(::(@belowVal, @lastline'), @x, @xs, @y) → newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y)
newline#2(nil, @x, @xs, @y) → nil
newline#3(@nl, @belowVal, @lastline', @x, @y) → newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y)
newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) → newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y)
newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) → newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl)
newline#6(@elem, @nl) → ::(@elem, @nl)
newline#7(#false, @belowVal, @diagVal, @rightVal) → max(@belowVal, @rightVal)
newline#7(#true, @belowVal, @diagVal, @rightVal) → +(@diagVal, #pos(#s(#0)))
right(@l) → right#1(@l)
right#1(::(@x, @xs)) → @x
right#1(nil) → #abs(#0)
The (relative) TRS S consists of the following rules:
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
firstline(::(@x311179_8, @xs311180_8)) →+ ::(#abs(#0), firstline(@xs311180_8))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@xs311180_8 / ::(@x311179_8, @xs311180_8)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)